Model Finding for Recursive Functions in SMT
Identifieur interne : 000441 ( Main/Exploration ); précédent : 000440; suivant : 000442Model Finding for Recursive Functions in SMT
Auteurs : Andrew Reynolds [Suisse] ; Jasmin Christian Blanchette [France] ; Cesare Tinelli [France, États-Unis]Source :
English descriptors
Abstract
SMT solvers have recently been extended with techniques for finding models in presence of universally quantified formulas in some restricted fragments. This paper introduces a translation which reduces axioms specifying a large class of recursive functions, including well-founded (terminating) functions, to universally quantified formulas for which these techniques are applicable. An empirical evaluation confirms that the approach improves the performance of existing solvers on benchmarks from two sources. The translation is implemented as a preprocessor in the solver CVC4.
Url:
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Hal, to step Corpus: 003249
- to stream Hal, to step Curation: 003249
- to stream Hal, to step Checkpoint: 000419
- to stream Main, to step Merge: 000441
- to stream Main, to step Curation: 000441
Le document en format XML
<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en">Model Finding for Recursive Functions in SMT</title><author><name sortKey="Reynolds, Andrew" sort="Reynolds, Andrew" uniqKey="Reynolds A" first="Andrew" last="Reynolds">Andrew Reynolds</name><affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-302851" status="VALID"><orgName>Ecole Polytechnique Fédérale de Lausanne</orgName><orgName type="acronym">EPFL</orgName><desc><address><addrLine>CH-1015 Lausanne Suisse Switzerland </addrLine><country key="CH"></country></address></desc></hal:affiliation><country>Suisse</country></affiliation></author><author><name sortKey="Blanchette, Jasmin Christian" sort="Blanchette, Jasmin Christian" uniqKey="Blanchette J" first="Jasmin Christian" last="Blanchette">Jasmin Christian Blanchette</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300009" type="direct"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-183914" status="VALID"><orgName>University of Iowa [Iowa]</orgName><desc><address><addrLine>Iowa City, IA 52242</addrLine><country key="FR"></country></address></desc><listRelation><relation active="#struct-366215" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-366215" type="direct"><org type="institution" xml:id="struct-366215" status="INCOMING"><orgName>University of Iowa</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Iowa City</settlement><region type="state">Iowa</region></placeName><country>États-Unis</country><orgName type="university">Université de l'Iowa</orgName></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">HAL</idno><idno type="RBID">Hal:hal-01242509</idno><idno type="halId">hal-01242509</idno><idno type="halUri">https://hal.inria.fr/hal-01242509</idno><idno type="url">https://hal.inria.fr/hal-01242509</idno><date when="2015-07-18">2015-07-18</date><idno type="wicri:Area/Hal/Corpus">003249</idno><idno type="wicri:Area/Hal/Curation">003249</idno><idno type="wicri:Area/Hal/Checkpoint">000419</idno><idno type="wicri:explorRef" wicri:stream="Hal" wicri:step="Checkpoint">000419</idno><idno type="wicri:Area/Main/Merge">000441</idno><idno type="wicri:Area/Main/Curation">000441</idno><idno type="wicri:Area/Main/Exploration">000441</idno></publicationStmt><sourceDesc><biblStruct><analytic><title xml:lang="en">Model Finding for Recursive Functions in SMT</title><author><name sortKey="Reynolds, Andrew" sort="Reynolds, Andrew" uniqKey="Reynolds A" first="Andrew" last="Reynolds">Andrew Reynolds</name><affiliation wicri:level="1"><hal:affiliation type="institution" xml:id="struct-302851" status="VALID"><orgName>Ecole Polytechnique Fédérale de Lausanne</orgName><orgName type="acronym">EPFL</orgName><desc><address><addrLine>CH-1015 Lausanne Suisse Switzerland </addrLine><country key="CH"></country></address></desc></hal:affiliation><country>Suisse</country></affiliation></author><author><name sortKey="Blanchette, Jasmin Christian" sort="Blanchette, Jasmin Christian" uniqKey="Blanchette J" first="Jasmin Christian" last="Blanchette">Jasmin Christian Blanchette</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-129671" status="VALID"><idno type="RNSR">198618246Y</idno><orgName>INRIA Nancy - Grand Est</orgName><desc><address><addrLine>615 rue du Jardin Botanique 54600 Villers-lès-Nancy</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/nancy</ref></desc><listRelation><relation active="#struct-300009" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-300009" type="direct"><org type="institution" xml:id="struct-300009" status="VALID"><orgName>Institut National de Recherche en Informatique et en Automatique</orgName><orgName type="acronym">Inria</orgName><desc><address><addrLine>Domaine de VoluceauRocquencourt - BP 10578153 Le Chesnay Cedex</addrLine><country key="FR"></country></address><ref type="url">http://www.inria.fr/en/</ref></desc></org></tutelle></tutelles></hal:affiliation><country>France</country></affiliation></author><author><name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name><affiliation wicri:level="1"><hal:affiliation type="laboratory" xml:id="struct-183914" status="VALID"><orgName>University of Iowa [Iowa]</orgName><desc><address><addrLine>Iowa City, IA 52242</addrLine><country key="FR"></country></address></desc><listRelation><relation active="#struct-366215" type="direct"></relation></listRelation><tutelles><tutelle active="#struct-366215" type="direct"><org type="institution" xml:id="struct-366215" status="INCOMING"><orgName>University of Iowa</orgName><desc><address><country key="FR"></country></address></desc></org></tutelle></tutelles></hal:affiliation><country>France</country><placeName><settlement type="city">Iowa City</settlement><region type="state">Iowa</region></placeName><country>États-Unis</country><orgName type="university">Université de l'Iowa</orgName></affiliation></author></analytic></biblStruct></sourceDesc></fileDesc><profileDesc><textClass><keywords scheme="mix" xml:lang="en"><term> counterexample generation</term><term> first-order logic</term><term> model finding</term><term>SMT solvers</term></keywords></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">SMT solvers have recently been extended with techniques for finding models in presence of universally quantified formulas in some restricted fragments. This paper introduces a translation which reduces axioms specifying a large class of recursive functions, including well-founded (terminating) functions, to universally quantified formulas for which these techniques are applicable. An empirical evaluation confirms that the approach improves the performance of existing solvers on benchmarks from two sources. The translation is implemented as a preprocessor in the solver CVC4.</div></front></TEI><affiliations><list><country><li>France</li><li>Suisse</li><li>États-Unis</li></country><region><li>Iowa</li></region><settlement><li>Iowa City</li></settlement><orgName><li>Université de l'Iowa</li></orgName></list><tree><country name="Suisse"><noRegion><name sortKey="Reynolds, Andrew" sort="Reynolds, Andrew" uniqKey="Reynolds A" first="Andrew" last="Reynolds">Andrew Reynolds</name></noRegion></country><country name="France"><noRegion><name sortKey="Blanchette, Jasmin Christian" sort="Blanchette, Jasmin Christian" uniqKey="Blanchette J" first="Jasmin Christian" last="Blanchette">Jasmin Christian Blanchette</name></noRegion><name sortKey="Tinelli, Cesare" sort="Tinelli, Cesare" uniqKey="Tinelli C" first="Cesare" last="Tinelli">Cesare Tinelli</name></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000441 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 000441 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= Hal:hal-01242509
|texte= Model Finding for Recursive Functions in SMT
}}
| This area was generated with Dilib version V0.6.33. |  |